Nuprl Lemma : eqmod_wf
2,24
postcript
pdf
m
,
a
,
b
:
. (
a
=
b
mod
m
)
Prop
latex
Definitions
a
=
b
mod
m
,
b
|
a
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
divides
wf
origin
m, a, b:
. (a = b mod m) 
Prop m, a, b:. (a = b mod m) Prop x:A. B(x) T